Left Termination of the query pattern map(b,f) w.r.t. the given Prolog program could successfully be proven:



↳ PROLOG
  ↳ PrologToPiTRSProof

p2(vali0, valj0).
map2(.2(X, Xs), .2(Y, Ys)) :- p2(X, Y), map2(Xs, Ys).
map2({}0, {}0).


With regard to the inferred argument filtering the predicates were used in the following modes:
map2: (b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


map_2_in_ga2(._22(X, Xs), ._22(Y, Ys)) -> if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
p_2_in_ga2(val_i_0, val_j_0) -> p_2_out_ga2(val_i_0, val_j_0)
if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
map_2_in_ga2([]_0, []_0) -> map_2_out_ga2([]_0, []_0)
if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_out_ga2(Xs, Ys)) -> map_2_out_ga2(._22(X, Xs), ._22(Y, Ys))

The argument filtering Pi contains the following mapping:
map_2_in_ga2(x1, x2)  =  map_2_in_ga1(x1)
val_i_0  =  val_i_0
val_j_0  =  val_j_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
if_map_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_1_ga2(x2, x5)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_map_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_2_ga2(x3, x5)
map_2_out_ga2(x1, x2)  =  map_2_out_ga1(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

map_2_in_ga2(._22(X, Xs), ._22(Y, Ys)) -> if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
p_2_in_ga2(val_i_0, val_j_0) -> p_2_out_ga2(val_i_0, val_j_0)
if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
map_2_in_ga2([]_0, []_0) -> map_2_out_ga2([]_0, []_0)
if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_out_ga2(Xs, Ys)) -> map_2_out_ga2(._22(X, Xs), ._22(Y, Ys))

The argument filtering Pi contains the following mapping:
map_2_in_ga2(x1, x2)  =  map_2_in_ga1(x1)
val_i_0  =  val_i_0
val_j_0  =  val_j_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
if_map_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_1_ga2(x2, x5)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_map_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_2_ga2(x3, x5)
map_2_out_ga2(x1, x2)  =  map_2_out_ga1(x2)


Pi DP problem:
The TRS P consists of the following rules:

MAP_2_IN_GA2(._22(X, Xs), ._22(Y, Ys)) -> IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
MAP_2_IN_GA2(._22(X, Xs), ._22(Y, Ys)) -> P_2_IN_GA2(X, Y)
IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> IF_MAP_2_IN_2_GA5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> MAP_2_IN_GA2(Xs, Ys)

The TRS R consists of the following rules:

map_2_in_ga2(._22(X, Xs), ._22(Y, Ys)) -> if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
p_2_in_ga2(val_i_0, val_j_0) -> p_2_out_ga2(val_i_0, val_j_0)
if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
map_2_in_ga2([]_0, []_0) -> map_2_out_ga2([]_0, []_0)
if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_out_ga2(Xs, Ys)) -> map_2_out_ga2(._22(X, Xs), ._22(Y, Ys))

The argument filtering Pi contains the following mapping:
map_2_in_ga2(x1, x2)  =  map_2_in_ga1(x1)
val_i_0  =  val_i_0
val_j_0  =  val_j_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
if_map_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_1_ga2(x2, x5)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_map_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_2_ga2(x3, x5)
map_2_out_ga2(x1, x2)  =  map_2_out_ga1(x2)
IF_MAP_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_MAP_2_IN_1_GA2(x2, x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
MAP_2_IN_GA2(x1, x2)  =  MAP_2_IN_GA1(x1)
IF_MAP_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_MAP_2_IN_2_GA2(x3, x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

MAP_2_IN_GA2(._22(X, Xs), ._22(Y, Ys)) -> IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
MAP_2_IN_GA2(._22(X, Xs), ._22(Y, Ys)) -> P_2_IN_GA2(X, Y)
IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> IF_MAP_2_IN_2_GA5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> MAP_2_IN_GA2(Xs, Ys)

The TRS R consists of the following rules:

map_2_in_ga2(._22(X, Xs), ._22(Y, Ys)) -> if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
p_2_in_ga2(val_i_0, val_j_0) -> p_2_out_ga2(val_i_0, val_j_0)
if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
map_2_in_ga2([]_0, []_0) -> map_2_out_ga2([]_0, []_0)
if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_out_ga2(Xs, Ys)) -> map_2_out_ga2(._22(X, Xs), ._22(Y, Ys))

The argument filtering Pi contains the following mapping:
map_2_in_ga2(x1, x2)  =  map_2_in_ga1(x1)
val_i_0  =  val_i_0
val_j_0  =  val_j_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
if_map_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_1_ga2(x2, x5)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_map_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_2_ga2(x3, x5)
map_2_out_ga2(x1, x2)  =  map_2_out_ga1(x2)
IF_MAP_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_MAP_2_IN_1_GA2(x2, x5)
P_2_IN_GA2(x1, x2)  =  P_2_IN_GA1(x1)
MAP_2_IN_GA2(x1, x2)  =  MAP_2_IN_GA1(x1)
IF_MAP_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_MAP_2_IN_2_GA2(x3, x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 2 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

MAP_2_IN_GA2(._22(X, Xs), ._22(Y, Ys)) -> IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> MAP_2_IN_GA2(Xs, Ys)

The TRS R consists of the following rules:

map_2_in_ga2(._22(X, Xs), ._22(Y, Ys)) -> if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
p_2_in_ga2(val_i_0, val_j_0) -> p_2_out_ga2(val_i_0, val_j_0)
if_map_2_in_1_ga5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_in_ga2(Xs, Ys))
map_2_in_ga2([]_0, []_0) -> map_2_out_ga2([]_0, []_0)
if_map_2_in_2_ga5(X, Xs, Y, Ys, map_2_out_ga2(Xs, Ys)) -> map_2_out_ga2(._22(X, Xs), ._22(Y, Ys))

The argument filtering Pi contains the following mapping:
map_2_in_ga2(x1, x2)  =  map_2_in_ga1(x1)
val_i_0  =  val_i_0
val_j_0  =  val_j_0
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
if_map_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_1_ga2(x2, x5)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
if_map_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_map_2_in_2_ga2(x3, x5)
map_2_out_ga2(x1, x2)  =  map_2_out_ga1(x2)
IF_MAP_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_MAP_2_IN_1_GA2(x2, x5)
MAP_2_IN_GA2(x1, x2)  =  MAP_2_IN_GA1(x1)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

MAP_2_IN_GA2(._22(X, Xs), ._22(Y, Ys)) -> IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_in_ga2(X, Y))
IF_MAP_2_IN_1_GA5(X, Xs, Y, Ys, p_2_out_ga2(X, Y)) -> MAP_2_IN_GA2(Xs, Ys)

The TRS R consists of the following rules:

p_2_in_ga2(val_i_0, val_j_0) -> p_2_out_ga2(val_i_0, val_j_0)

The argument filtering Pi contains the following mapping:
val_i_0  =  val_i_0
val_j_0  =  val_j_0
._22(x1, x2)  =  ._22(x1, x2)
p_2_in_ga2(x1, x2)  =  p_2_in_ga1(x1)
p_2_out_ga2(x1, x2)  =  p_2_out_ga1(x2)
IF_MAP_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_MAP_2_IN_1_GA2(x2, x5)
MAP_2_IN_GA2(x1, x2)  =  MAP_2_IN_GA1(x1)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

MAP_2_IN_GA1(._22(X, Xs)) -> IF_MAP_2_IN_1_GA2(Xs, p_2_in_ga1(X))
IF_MAP_2_IN_1_GA2(Xs, p_2_out_ga1(Y)) -> MAP_2_IN_GA1(Xs)

The TRS R consists of the following rules:

p_2_in_ga1(val_i_0) -> p_2_out_ga1(val_j_0)

The set Q consists of the following terms:

p_2_in_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_MAP_2_IN_1_GA2, MAP_2_IN_GA1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: